Nuprl Definition : Rda 11,40
Rda(R)
== es_realizer_ind(R;
== es_realizer_ind(fpf-empty;
== es_realizer_ind(left,right,rec1,rec2.fpf-empty;
== es_realizer_ind(loc,T,x,v.fpf-empty;
== es_realizer_ind(loc,T,x,L.fpf-empty;
== es_realizer_ind(lnk,tag,L.fpf-empty;
== es_realizer_ind(loc,ds,knd,T,x,f.fpf-single(knd; T);
== es_realizer_ind(ds,knd,T,l,dt,g.fpf-join(Kind-deq; fpf-single(knd; T); lnk-decl(l; dt));
== es_realizer_ind(loc,ds,a,p,P.fpf-single(locl(a); p-outcome(p));
== es_realizer_ind(loc,k,L.fpf-empty;
== es_realizer_ind(loc,k,L.fpf-empty;
== es_realizer_ind(loc,x,L.fpf-empty) 
latex

Definitionsfpf-empty, p-outcome(p), locl(a), fpf-single(x; v), lnk-decl(l; dt), Kind-deq, fpf-join(eq; f; g), es realizer ind
FDL editor aliasesRda

origin